ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-halt-kind(x)  Knd+Unit 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, ecl(ds;da), , type List, Unit, left+right, , inr(x), , Valtype(da;k), x:AB(x), State(ds), inl(x), x,y,z. t(x;y;z), x,y. t(x;y), x,y,z,w. t(x;y;z;w), ecl ind, ecl-halt-kind(x)
Lemmas	ecl ind wf, decl-state wf, ma-valtype wf, bool wf, it wf, unit wf, nat wf, ecl wf, Knd wf, fpf wf, Id wf